x, y:Top List, b:. null(if b x else y fi) = if b null(x) else null(y) fi   

latex

Definitions	t  T, Top, x:A. B(x), null(as), b, A, b, , Prop, P  Q, P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, null wf, top wf